To allow non-integral flows we should define flows on more general types.
Perhaps {α : Type*} [AddGroup α] [LE α] for the definition, and most lemmas would require [LinearOrder α]? I'm not sure what's the best choice here.
The capacities can have the same type as the values, and capacity will enforce they are non-negative.

Agreed that an α-valued Flow might be nicer API, but for now I would like to keep ℤ/ℕ because the next step is strong MFMC (and Menger), where integrality/termination arguments are way simpler. Happy to follow up with a separate PR generalizing the definition + weak duality once the core theorem lands. I think at this point generalizing would unnecessarily increase the overhead of mechanizing a lot of the core results in graph theory, but let me know what you think.

Umm that depends. Do you prefer splitting because it'll be easier to review, or because you did not prove the general case and prefer to leave generalizing as a TODO? Both are good reasons to not generalize now, but "integrality/termination arguments are way simpler" confuses me.
If it's neither of these (e.g. you already proved the general case but want to PR the special case first and then replace it entirely) then I don't see a reason to do this.

Either way I think having both ℤ/ℕ complicates things (adds casts and makes this not a special case of the general case), wdyt about using integer capacities? Non-negativity is already enforced.

Yeah sorry, my phrasing was sloppy. The reason I’m not generalizing to α in this PR is that I haven’t proved the α-valued development yet so it would basically be leaving a design-heavy TODO, and my next planned step is strong MFMC via an augmenting-path/Ford–Fulkerson style proof, where working integrally makes the termination/integrality story much cleaner, and also lines up with the Menger corollary later. Agreed about the ℤ/ℕ mix: I’ve updated the code to use integer capacities (c : Sym2 V -> ℤ). Thanks for the suggestion.

If the problem is strong MFMC, can you generalize the Flow stuff here, and just in your proof of strong MFMC take in a Flow ℤ?

btw wouldn't a proof using LP duality work? I imagine it's much cleaner since we don't need any algorithmic proof + termination, and it should work for the general case.

I agree, I’ve generalized the definitions/weak duality so Flow takes values in α and capacities are c : Sym2 V -> α (so no casts and this covers non-integral flows). You're right that can prove strong MFMC by specializing to α := ℤ. Re LP duality, I just saw that Mathlib/Analysis/Convex/Cone/Basic.lean discusses Farkas/conic duality and explicitly lists LP duality as a TODO, i.e, it seems like the main underlying infrastructure would be lacking there. But if you think that avenue would lead to overall cleaner code I'm happy to do it that way.